nLab seven trees in one

Idea

There is a natural bijection between the set of finite binary trees and the set of seven-tuples of such.

This observation, originally made by Bill Lawvere, has since then been expanded to other “polynomial equations” apart from $T \simeq T^7$ and other types than trees, revealing connections between type theory and calculus.

References

• John Baez, this week’s finds in mathematical physics, week 202, web

• Andreas Blass, seven trees in one, arXiv:math/9405205v1

• Tom Leinster, objects of categories as complex numbers, arXiv:math/0212377v1

category: type theory, formal calculus